\begin{tabbing} $\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:Id, $T$:Type, ${\it ks}$:Knd List,\+ \\[0ex]$a$:($\mathbb{N}\rightarrow$($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$) \}$\rightarrow$State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$$T$$\rightarrow\mathbb{B}$)), ${\it snd}$:msg{-}spec(${\it ds}$;${\it da}$). \-\\[0ex]$\neg$$x$ $\in$ dom(${\it ds}$) $\Rightarrow$ ecl{-}machine3(${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it snd}$) $\in$ Realizer \end{tabbing}